// SPDX-License-Identifier: GPL-2.0 or GPL-3.0
// Copyright © 2019 Ariadne Devos

#ifndef _sHT_STRING_SETOPS_H
#define _sHT_STRING_SETOPS_H

#include <stddef.h>
#include <stdint.h>

/* TODO: 'reads' clauses */

/*@ predicate memeq16{L1, L2}(uint16_t *v0, uint16_t *v1, ℤ n) =
      \forall ℤ j; 0 <= j < n ==> \at(v0[j], L1) == \at(v1[j], L2); */

/*@ predicate bzero16{L1}(uint16_t *v, ℤ n) =
      \forall ℤ j; 0 <= j < n ==> \at(v[j], L1) == 0; */

/*@ requires dest_w: \valid(dest + (0 .. e0 - 1));
    requires dest_w0S: \valid(dest + 0);
    requires from_r: \valid_read(from + (0 .. b1 + (e0 - b0) - 1));
    requires from_s: \initialized(from + (0 .. b1 + (e0 - b0) - 1));
    requires from_r0S: \valid_read(from + 0);
    requires from_s0S: \initialized(from + 0);
    requires d: \separated(dest + (0 .. e0 - 1), from + (0 .. b1 + (e0 - b0) - 1));
    requires rd: b0 <= e0;
    requires rf: b1 <= b1 + (e0 - b0) <= SIZE_MAX;
    terminates \true;
    // assignsS dest[0], dest[0 .. e0 - 1] \from from[0], from[0 .. b1 + (e0 - b0) - 1];
    assigns dest[b0 .. e0 - 1] \from from[b0 .. b1 + (e0 - b0) - 1];
    ensures dest_sNS: \initialized(dest + (b0 .. e0 - 1));
    ensures copyNS: memeq16{Post,Pre}(dest + b0, from + b1, e0 - b0); */
void
sHT_memcpy16_r2(uint16_t dest[], uint16_t from[], size_t e0, size_t b0, size_t b1);

/* TODO: special cases (e.g., ARM has 128-bit vectors, hint IPv6?,
   more alignment?). */
/*@ requires dest_w: \valid(dest + (0 .. e - 1));
    requires dest_w0S: \valid(dest + 0);
    requires order: b <= e;
    terminates \true;
    // assignsS dest[0], dest[0 .. e - 1] \from \nothing;
    assigns dest[b .. e - 1] \from \nothing;
    ensures dest_sS: \initialized(dest + (0 .. e - 1));
    ensures zeroNS: bzero16{Post}(dest + b, e - b); */
void
sHT_bzero16_r1(uint16_t dest[], size_t e, size_t b);

#endif
